The goal of this study was to investigate approaches to 'high- assurance' software written in the Ada programming language. 'High-assurance' software is an expression used throughout this report that includes the software in systems defined to be secure by the Department of Defense Trusted Computer System Evaluation Criteria as well as other software with very high reliability or security requirements. 'High-assurance' software includes any software which must function as intended or there would be a threat to human life or national security. The report is applicable, then, to high-assurance software which, for the most part, is yet to be developed. Secure communications.